\begin{tabbing}
($\backslash$p\=.let A = get\_term\_arg `A` p \+
\\[0ex]in let x = get\_term\_arg `x` p 
\\[0ex]
\\[0ex]in let e = get\_term\_arg `e` p 
\\[0ex]i\=n \+
\\[0ex]At (get\_term\_arg `UH` p) 
\\[0ex](Sub\=st \+
\\[0ex]
\\[0ex](\=mk\_equal\_term \+
\\[0ex](mk\_set\_term (dv x) A (mk\_equal\_term A e x)) 
\\[0ex]e
\\[0ex]
\\[0ex]x) 
\-\\[0ex](get\_int\_arg `i` p + 2)) p)
\-\-\-
\end{tabbing}